\documentstyle[12pt,a4,jrh,alltt,proof]{book2}

\input epsf

\title{\Huge \bf Introduction to Functional Programming}

\author{\Large {\bf John Harrison}\\{\tt jrh@cl.cam.ac.uk}}

\date{3rd December 1997}

\input amssym.def
\input amssym

\input epsf

\newcommand{\nat}{\mbox{$\protect\Bbb N$}}
\newcommand{\num}{\mbox{$\protect\Bbb Z$}}
\newcommand{\rat}{\mbox{$\protect\Bbb Q$}}
\newcommand{\real}{\mbox{$\protect\Bbb R$}}
\newcommand{\complex}{\mbox{$\protect\Bbb C$}}
\newcommand{\xxx}{\mbox{$\protect\Bbb X$}}

\newcommand{\lamb}[1]{\lambda #1.\:}
\newcommand{\eps}[1]{\varepsilon #1.\:}
\newcommand{\all}[1]{\forall #1.\:}
\newcommand{\ex}[1]{\exists #1.\:}
\newcommand{\exu}[1]{\exists! #1.\:}

\newcommand{\True}{\top}
\newcommand{\False}{\bot}
\newcommand{\Not}{\neg}
\newcommand{\And}{\wedge}
\newcommand{\Or}{\vee}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}

\newcommand{\entails}{\vdash}
\newcommand{\proves}{\vdash}

\newcommand{\Ands}{\bigwedge}
\newcommand{\Ors}{\bigvee}

\newcommand{\BQ}{\mbox{$\ulcorner$}}
\newcommand{\BEQ}{\mbox{\raise4pt\hbox{$\ulcorner$}}}
\newcommand{\EQ}{\mbox{$\urcorner$}}
\newcommand{\EEQ}{\mbox{\raise4pt\hbox{$\urcorner$}}}

\newcommand{\QUOTE}[1]{\mbox{$\BQ #1 \EQ$}}

\let\psubset=\subset                    % Pure TeX: thanks to MAJ %
\let\subset=\subseteq

\newcommand{\powerset}{\wp}             % This is pretty dire...  %

\newcommand{\Union}{\cup}
\newcommand{\Inter}{\cap}
\newcommand{\Unions}{\bigcup}
\newcommand{\Inters}{\bigcap}

\newcommand{\proof}{{\bf \noindent Proof:\ }}
\newcommand{\qed}{Q.E.D.}

\newcommand{\Rule}{\infer}

\newcommand{\restrict}{\upharpoonright} % This is lousy and must be fixed! %

\newcommand{\bigsqcap}{\mbox{\Large{$\sqcap$}}}

\newcommand\leb{\lbrack\!\lbrack}
\newcommand\reb{\rbrack\!\rbrack}
\newcommand{\sem}[1]{\leb #1 \reb}

\newcommand{\BA}{\begin{array}[t]{l}}
\newcommand{\EA}{\end{array}}

\newcommand{\sqle}{\sqsubseteq}
\newcommand{\sqlt}{\sqsubset}

\newcommand{\too}{\twoheadrightarrow}

\newcommand{\Los}{{\L}o{\'s}}

\newcommand{\defeq}{\stackrel{\bigtriangleup}{=}}

\def\alphas{\mathrel{\mathop{\longrightarrow}\limits_{\alpha}}}
\def\betas{\mathrel{\mathop{\longrightarrow}\limits_{\beta}}}
\def\etas{\mathrel{\mathop{\longrightarrow}\limits_{\eta}}}

\def\goesto{\longrightarrow}

\begin{document}

\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

% This is stuff for boxes, stolen from HOL documentation

\newcommand\HOLSpacing{12pt}

\newlength{\hsbw}
\setlength{\hsbw}{\textwidth}
\addtolength{\hsbw}{-\arrayrulewidth}
\addtolength{\hsbw}{-\tabcolsep}

\newenvironment{boxed}{\begin{flushleft}
 \begin{tabular}{@{}|c@{}|@{}}\hline
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline
 \end{tabular}
 \end{flushleft}}

\maketitle

\pagenumbering{roman}

%\centerline{\epsffile{caml-inside.ps}}

\vspace{12in}
\begin{center}
%{\Large \em To my students, past and present}
\end{center}

\pagebreak

\input preface.tex
\input plan.tex

\tableofcontents

\vfill

\pagebreak

\pagenumbering{arabic}

\input intro.tex
\input lamb.tex
\input prog.tex
\input types.tex
\input ml.tex
\input fml.tex
\input proving.tex
\input effect.tex
\input examples.tex

\bibliographystyle{jrh}

\bibliography{all}

\end{document}
